Runtime Complexity (innermost) proof of /tmp/tmpEYgiGG/PEANO_nosorts_noand

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 88 ms)

↳2 CdtProblem

    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳4 CdtProblem

    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 11 ms)

    ↳8 CdtProblem

    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳10 CdtProblem

    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳12 CdtProblem

    ↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳14 CdtProblem

    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳16 CdtProblem

    ↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳22 CdtProblem

↳23 CpxTrsMatchBoundsTAProof (⇔, 37 ms)

↳24 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
mark(U11(X1, X2, X3)) → active(U11(mark(X1), X2, X3))
mark(tt) → active(tt)
mark(U12(X1, X2, X3)) → active(U12(mark(X1), X2, X3))
mark(s(X)) → active(s(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
U11(mark(X1), X2, X3) → U11(X1, X2, X3)
U11(X1, mark(X2), X3) → U11(X1, X2, X3)
U11(X1, X2, mark(X3)) → U11(X1, X2, X3)
U11(active(X1), X2, X3) → U11(X1, X2, X3)
U11(X1, active(X2), X3) → U11(X1, X2, X3)
U11(X1, X2, active(X3)) → U11(X1, X2, X3)
U12(mark(X1), X2, X3) → U12(X1, X2, X3)
U12(X1, mark(X2), X3) → U12(X1, X2, X3)
U12(X1, X2, mark(X3)) → U12(X1, X2, X3)
U12(active(X1), X2, X3) → U12(X1, X2, X3)
U12(X1, active(X2), X3) → U12(X1, X2, X3)
U12(X1, X2, active(X3)) → U12(X1, X2, X3)
s(mark(X)) → s(X)
s(active(X)) → s(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(U12(tt, z0, z1)) → c1(MARK(s(plus(z1, z0))), S(plus(z1, z0)), PLUS(z1, z0))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(mark(z0), z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(tt) → c5(ACTIVE(tt))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(0) → c9(ACTIVE(0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(U12(tt, z0, z1)) → c1(MARK(s(plus(z1, z0))), S(plus(z1, z0)), PLUS(z1, z0))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(mark(z0), z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(tt) → c5(ACTIVE(tt))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(0) → c9(ACTIVE(0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, MARK, U11', U12', S, PLUS

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

MARK(tt) → c5(ACTIVE(tt))
MARK(0) → c9(ACTIVE(0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(U12(tt, z0, z1)) → c1(MARK(s(plus(z1, z0))), S(plus(z1, z0)), PLUS(z1, z0))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(mark(z0), z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(U12(tt, z0, z1)) → c1(MARK(s(plus(z1, z0))), S(plus(z1, z0)), PLUS(z1, z0))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(mark(z0), z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, MARK, U11', U12', S, PLUS

Compound Symbols:

c, c1, c2, c3, c4, c6, c7, c8, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(U12(tt, z0, z1)) → c1(MARK(s(plus(z1, z0))), S(plus(z1, z0)), PLUS(z1, z0)) by

ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(mark(z0), z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(mark(z0), z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, MARK, U11', U12', S, PLUS

Compound Symbols:

c, c2, c3, c4, c6, c7, c8, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(mark(z0), z1, z2)), U11'(mark(z0), z1, z2), MARK(z0)) by

MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, MARK, U11', U12', S, PLUS

Compound Symbols:

c, c2, c3, c6, c7, c8, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1, c4, c4

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(mark(z0), z1, z2)), U12'(mark(z0), z1, z2), MARK(z0)) by

MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, MARK, U11', U12', S, PLUS

Compound Symbols:

c, c2, c3, c7, c8, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1, c4, c4, c6, c6

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0)) by

MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(x0)) → c7

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(x0)) → c7

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(x0)) → c7

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, MARK, U11', U12', S, PLUS

Compound Symbols:

c, c2, c3, c8, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1, c4, c4, c6, c6, c7, c7

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(s(x0)) → c7

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, MARK, U11', U12', S, PLUS

Compound Symbols:

c, c2, c3, c8, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1, c4, c4, c6, c6, c7

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(plus(z0, z1)) → c8(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1)) by

MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(x0, x1)) → c8

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(x0, x1)) → c8

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(x0, x1)) → c8

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, U11', U12', S, PLUS, MARK

Compound Symbols:

c, c2, c3, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1, c4, c4, c6, c6, c7, c8, c8

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(plus(x0, x1)) → c8

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, U11', U12', S, PLUS, MARK

Compound Symbols:

c, c2, c3, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1, c4, c4, c6, c6, c7, c8

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(U11(U11(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U11(mark(z0), z1, z2)), x1, x2)), U11'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2))) by

MARK(U11(U11(x0, x1, x2), z1, z2)) → c4(ACTIVE(U11(U11(mark(x0), x1, x2), z1, z2)), U11'(mark(U11(x0, x1, x2)), z1, z2), MARK(U11(x0, x1, x2)))
MARK(U11(U11(z0, z1, z2), x3, x4)) → c4(ACTIVE(U11(active(U11(z0, z1, z2)), x3, x4)), U11'(mark(U11(z0, z1, z2)), x3, x4), MARK(U11(z0, z1, z2)))
MARK(U11(U11(U11(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U11(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U11(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U11(z0, z1, z2), x1, x2)))
MARK(U11(U11(tt, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(tt), x1, x2)), x3, x4)), U11'(mark(U11(tt, x1, x2)), x3, x4), MARK(U11(tt, x1, x2)))
MARK(U11(U11(U12(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U12(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U12(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U12(z0, z1, z2), x1, x2)))
MARK(U11(U11(s(z0), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(s(mark(z0))), x1, x2)), x3, x4)), U11'(mark(U11(s(z0), x1, x2)), x3, x4), MARK(U11(s(z0), x1, x2)))
MARK(U11(U11(plus(z0, z1), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(plus(mark(z0), mark(z1))), x1, x2)), x3, x4)), U11'(mark(U11(plus(z0, z1), x1, x2)), x3, x4), MARK(U11(plus(z0, z1), x1, x2)))
MARK(U11(U11(0, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(0), x1, x2)), x3, x4)), U11'(mark(U11(0, x1, x2)), x3, x4), MARK(U11(0, x1, x2)))
MARK(U11(U11(x0, x1, x2), x3, x4)) → c4(U11'(mark(U11(x0, x1, x2)), x3, x4))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(U11(U11(x0, x1, x2), z1, z2)) → c4(ACTIVE(U11(U11(mark(x0), x1, x2), z1, z2)), U11'(mark(U11(x0, x1, x2)), z1, z2), MARK(U11(x0, x1, x2)))
MARK(U11(U11(z0, z1, z2), x3, x4)) → c4(ACTIVE(U11(active(U11(z0, z1, z2)), x3, x4)), U11'(mark(U11(z0, z1, z2)), x3, x4), MARK(U11(z0, z1, z2)))
MARK(U11(U11(U11(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U11(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U11(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U11(z0, z1, z2), x1, x2)))
MARK(U11(U11(tt, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(tt), x1, x2)), x3, x4)), U11'(mark(U11(tt, x1, x2)), x3, x4), MARK(U11(tt, x1, x2)))
MARK(U11(U11(U12(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U12(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U12(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U12(z0, z1, z2), x1, x2)))
MARK(U11(U11(s(z0), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(s(mark(z0))), x1, x2)), x3, x4)), U11'(mark(U11(s(z0), x1, x2)), x3, x4), MARK(U11(s(z0), x1, x2)))
MARK(U11(U11(plus(z0, z1), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(plus(mark(z0), mark(z1))), x1, x2)), x3, x4)), U11'(mark(U11(plus(z0, z1), x1, x2)), x3, x4), MARK(U11(plus(z0, z1), x1, x2)))
MARK(U11(U11(0, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(0), x1, x2)), x3, x4)), U11'(mark(U11(0, x1, x2)), x3, x4), MARK(U11(0, x1, x2)))
MARK(U11(U11(x0, x1, x2), x3, x4)) → c4(U11'(mark(U11(x0, x1, x2)), x3, x4))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(U11(U11(x0, x1, x2), z1, z2)) → c4(ACTIVE(U11(U11(mark(x0), x1, x2), z1, z2)), U11'(mark(U11(x0, x1, x2)), z1, z2), MARK(U11(x0, x1, x2)))
MARK(U11(U11(z0, z1, z2), x3, x4)) → c4(ACTIVE(U11(active(U11(z0, z1, z2)), x3, x4)), U11'(mark(U11(z0, z1, z2)), x3, x4), MARK(U11(z0, z1, z2)))
MARK(U11(U11(U11(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U11(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U11(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U11(z0, z1, z2), x1, x2)))
MARK(U11(U11(tt, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(tt), x1, x2)), x3, x4)), U11'(mark(U11(tt, x1, x2)), x3, x4), MARK(U11(tt, x1, x2)))
MARK(U11(U11(U12(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U12(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U12(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U12(z0, z1, z2), x1, x2)))
MARK(U11(U11(s(z0), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(s(mark(z0))), x1, x2)), x3, x4)), U11'(mark(U11(s(z0), x1, x2)), x3, x4), MARK(U11(s(z0), x1, x2)))
MARK(U11(U11(plus(z0, z1), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(plus(mark(z0), mark(z1))), x1, x2)), x3, x4)), U11'(mark(U11(plus(z0, z1), x1, x2)), x3, x4), MARK(U11(plus(z0, z1), x1, x2)))
MARK(U11(U11(0, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(0), x1, x2)), x3, x4)), U11'(mark(U11(0, x1, x2)), x3, x4), MARK(U11(0, x1, x2)))
MARK(U11(U11(x0, x1, x2), x3, x4)) → c4(U11'(mark(U11(x0, x1, x2)), x3, x4))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, U11', U12', S, PLUS, MARK

Compound Symbols:

c, c2, c3, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1, c4, c4, c6, c6, c7, c8

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(U11(tt, x1, x2)) → c4(ACTIVE(U11(active(tt), x1, x2)), U11'(mark(tt), x1, x2), MARK(tt)) by

MARK(U11(tt, z1, z2)) → c4(ACTIVE(U11(tt, z1, z2)), U11'(mark(tt), z1, z2), MARK(tt))
MARK(U11(tt, x0, x1)) → c4(U11'(mark(tt), x0, x1))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(U11(tt, z0, z1)) → mark(U12(tt, z0, z1))
active(U12(tt, z0, z1)) → mark(s(plus(z1, z0)))
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(U11(tt, z1, z0))
mark(U11(z0, z1, z2)) → active(U11(mark(z0), z1, z2))
mark(tt) → active(tt)
mark(U12(z0, z1, z2)) → active(U12(mark(z0), z1, z2))
mark(s(z0)) → active(s(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
U11(mark(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, mark(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, mark(z2)) → U11(z0, z1, z2)
U11(active(z0), z1, z2) → U11(z0, z1, z2)
U11(z0, active(z1), z2) → U11(z0, z1, z2)
U11(z0, z1, active(z2)) → U11(z0, z1, z2)
U12(mark(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, mark(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, mark(z2)) → U12(z0, z1, z2)
U12(active(z0), z1, z2) → U12(z0, z1, z2)
U12(z0, active(z1), z2) → U12(z0, z1, z2)
U12(z0, z1, active(z2)) → U12(z0, z1, z2)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)

Tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(U11(U11(x0, x1, x2), z1, z2)) → c4(ACTIVE(U11(U11(mark(x0), x1, x2), z1, z2)), U11'(mark(U11(x0, x1, x2)), z1, z2), MARK(U11(x0, x1, x2)))
MARK(U11(U11(z0, z1, z2), x3, x4)) → c4(ACTIVE(U11(active(U11(z0, z1, z2)), x3, x4)), U11'(mark(U11(z0, z1, z2)), x3, x4), MARK(U11(z0, z1, z2)))
MARK(U11(U11(U11(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U11(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U11(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U11(z0, z1, z2), x1, x2)))
MARK(U11(U11(tt, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(tt), x1, x2)), x3, x4)), U11'(mark(U11(tt, x1, x2)), x3, x4), MARK(U11(tt, x1, x2)))
MARK(U11(U11(U12(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U12(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U12(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U12(z0, z1, z2), x1, x2)))
MARK(U11(U11(s(z0), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(s(mark(z0))), x1, x2)), x3, x4)), U11'(mark(U11(s(z0), x1, x2)), x3, x4), MARK(U11(s(z0), x1, x2)))
MARK(U11(U11(plus(z0, z1), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(plus(mark(z0), mark(z1))), x1, x2)), x3, x4)), U11'(mark(U11(plus(z0, z1), x1, x2)), x3, x4), MARK(U11(plus(z0, z1), x1, x2)))
MARK(U11(U11(0, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(0), x1, x2)), x3, x4)), U11'(mark(U11(0, x1, x2)), x3, x4), MARK(U11(0, x1, x2)))
MARK(U11(U11(x0, x1, x2), x3, x4)) → c4(U11'(mark(U11(x0, x1, x2)), x3, x4))
MARK(U11(tt, z1, z2)) → c4(ACTIVE(U11(tt, z1, z2)), U11'(mark(tt), z1, z2), MARK(tt))
MARK(U11(tt, x0, x1)) → c4(U11'(mark(tt), x0, x1))

S tuples:

ACTIVE(U11(tt, z0, z1)) → c(MARK(U12(tt, z0, z1)), U12'(tt, z0, z1))
ACTIVE(plus(z0, 0)) → c2(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c3(MARK(U11(tt, z1, z0)), U11'(tt, z1, z0))
U11'(mark(z0), z1, z2) → c10(U11'(z0, z1, z2))
U11'(z0, mark(z1), z2) → c11(U11'(z0, z1, z2))
U11'(z0, z1, mark(z2)) → c12(U11'(z0, z1, z2))
U11'(active(z0), z1, z2) → c13(U11'(z0, z1, z2))
U11'(z0, active(z1), z2) → c14(U11'(z0, z1, z2))
U11'(z0, z1, active(z2)) → c15(U11'(z0, z1, z2))
U12'(mark(z0), z1, z2) → c16(U12'(z0, z1, z2))
U12'(z0, mark(z1), z2) → c17(U12'(z0, z1, z2))
U12'(z0, z1, mark(z2)) → c18(U12'(z0, z1, z2))
U12'(active(z0), z1, z2) → c19(U12'(z0, z1, z2))
U12'(z0, active(z1), z2) → c20(U12'(z0, z1, z2))
U12'(z0, z1, active(z2)) → c21(U12'(z0, z1, z2))
S(mark(z0)) → c22(S(z0))
S(active(z0)) → c23(S(z0))
PLUS(mark(z0), z1) → c24(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c25(PLUS(z0, z1))
PLUS(active(z0), z1) → c26(PLUS(z0, z1))
PLUS(z0, active(z1)) → c27(PLUS(z0, z1))
ACTIVE(U12(tt, x0, x1)) → c1(MARK(s(plus(x1, x0))), PLUS(x1, x0))
MARK(U11(z0, z1, z2)) → c4(ACTIVE(U11(z0, z1, z2)), U11'(mark(z0), z1, z2), MARK(z0))
MARK(U11(U12(z0, z1, z2), x1, x2)) → c4(ACTIVE(U11(active(U12(mark(z0), z1, z2)), x1, x2)), U11'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U11(s(z0), x1, x2)) → c4(ACTIVE(U11(active(s(mark(z0))), x1, x2)), U11'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U11(plus(z0, z1), x1, x2)) → c4(ACTIVE(U11(active(plus(mark(z0), mark(z1))), x1, x2)), U11'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U11(0, x1, x2)) → c4(ACTIVE(U11(active(0), x1, x2)), U11'(mark(0), x1, x2), MARK(0))
MARK(U11(x0, x1, x2)) → c4(U11'(mark(x0), x1, x2))
MARK(U12(z0, z1, z2)) → c6(ACTIVE(U12(z0, z1, z2)), U12'(mark(z0), z1, z2), MARK(z0))
MARK(U12(U11(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U11(mark(z0), z1, z2)), x1, x2)), U12'(mark(U11(z0, z1, z2)), x1, x2), MARK(U11(z0, z1, z2)))
MARK(U12(tt, x1, x2)) → c6(ACTIVE(U12(active(tt), x1, x2)), U12'(mark(tt), x1, x2), MARK(tt))
MARK(U12(U12(z0, z1, z2), x1, x2)) → c6(ACTIVE(U12(active(U12(mark(z0), z1, z2)), x1, x2)), U12'(mark(U12(z0, z1, z2)), x1, x2), MARK(U12(z0, z1, z2)))
MARK(U12(s(z0), x1, x2)) → c6(ACTIVE(U12(active(s(mark(z0))), x1, x2)), U12'(mark(s(z0)), x1, x2), MARK(s(z0)))
MARK(U12(plus(z0, z1), x1, x2)) → c6(ACTIVE(U12(active(plus(mark(z0), mark(z1))), x1, x2)), U12'(mark(plus(z0, z1)), x1, x2), MARK(plus(z0, z1)))
MARK(U12(0, x1, x2)) → c6(ACTIVE(U12(active(0), x1, x2)), U12'(mark(0), x1, x2), MARK(0))
MARK(U12(x0, x1, x2)) → c6(U12'(mark(x0), x1, x2))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(U11(z0, z1, z2))) → c7(ACTIVE(s(active(U11(mark(z0), z1, z2)))), S(mark(U11(z0, z1, z2))), MARK(U11(z0, z1, z2)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(U12(z0, z1, z2))) → c7(ACTIVE(s(active(U12(mark(z0), z1, z2)))), S(mark(U12(z0, z1, z2))), MARK(U12(z0, z1, z2)))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(plus(z0, x1)) → c8(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c8(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, U11(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U11(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U11(z0, z1, z2))), MARK(x0), MARK(U11(z0, z1, z2)))
MARK(plus(x0, tt)) → c8(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, U12(z0, z1, z2))) → c8(ACTIVE(plus(mark(x0), active(U12(mark(z0), z1, z2)))), PLUS(mark(x0), mark(U12(z0, z1, z2))), MARK(x0), MARK(U12(z0, z1, z2)))
MARK(plus(x0, s(z0))) → c8(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(x0, plus(z0, z1))) → c8(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c8(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(U11(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U11(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U11(z0, z1, z2)), mark(x1)), MARK(U11(z0, z1, z2)), MARK(x1))
MARK(plus(tt, x1)) → c8(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(U12(z0, z1, z2), x1)) → c8(ACTIVE(plus(active(U12(mark(z0), z1, z2)), mark(x1))), PLUS(mark(U12(z0, z1, z2)), mark(x1)), MARK(U12(z0, z1, z2)), MARK(x1))
MARK(plus(s(z0), x1)) → c8(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c8(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c8(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(U11(U11(x0, x1, x2), z1, z2)) → c4(ACTIVE(U11(U11(mark(x0), x1, x2), z1, z2)), U11'(mark(U11(x0, x1, x2)), z1, z2), MARK(U11(x0, x1, x2)))
MARK(U11(U11(z0, z1, z2), x3, x4)) → c4(ACTIVE(U11(active(U11(z0, z1, z2)), x3, x4)), U11'(mark(U11(z0, z1, z2)), x3, x4), MARK(U11(z0, z1, z2)))
MARK(U11(U11(U11(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U11(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U11(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U11(z0, z1, z2), x1, x2)))
MARK(U11(U11(tt, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(tt), x1, x2)), x3, x4)), U11'(mark(U11(tt, x1, x2)), x3, x4), MARK(U11(tt, x1, x2)))
MARK(U11(U11(U12(z0, z1, z2), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(U12(mark(z0), z1, z2)), x1, x2)), x3, x4)), U11'(mark(U11(U12(z0, z1, z2), x1, x2)), x3, x4), MARK(U11(U12(z0, z1, z2), x1, x2)))
MARK(U11(U11(s(z0), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(s(mark(z0))), x1, x2)), x3, x4)), U11'(mark(U11(s(z0), x1, x2)), x3, x4), MARK(U11(s(z0), x1, x2)))
MARK(U11(U11(plus(z0, z1), x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(plus(mark(z0), mark(z1))), x1, x2)), x3, x4)), U11'(mark(U11(plus(z0, z1), x1, x2)), x3, x4), MARK(U11(plus(z0, z1), x1, x2)))
MARK(U11(U11(0, x1, x2), x3, x4)) → c4(ACTIVE(U11(active(U11(active(0), x1, x2)), x3, x4)), U11'(mark(U11(0, x1, x2)), x3, x4), MARK(U11(0, x1, x2)))
MARK(U11(U11(x0, x1, x2), x3, x4)) → c4(U11'(mark(U11(x0, x1, x2)), x3, x4))
MARK(U11(tt, z1, z2)) → c4(ACTIVE(U11(tt, z1, z2)), U11'(mark(tt), z1, z2), MARK(tt))
MARK(U11(tt, x0, x1)) → c4(U11'(mark(tt), x0, x1))

K tuples:none
Defined Rule Symbols:

active, mark, U11, U12, s, plus

Defined Pair Symbols:

ACTIVE, U11', U12', S, PLUS, MARK

Compound Symbols:

c, c2, c3, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c1, c4, c4, c6, c6, c7, c8

(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6]
transitions:
tt0() → 0
00() → 0
active0(0) → 1
mark0(0) → 2
U110(0, 0, 0) → 3
U120(0, 0, 0) → 4
s0(0) → 5
plus0(0, 0) → 6
tt1() → 7
active1(7) → 2
01() → 8
active1(8) → 2

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

(24) BOUNDS(O(1), O(n^1))